$\forall$$T$:Type, $E$:($T$$\rightarrow$$T$$\rightarrow$Prop), $x$, $y$:$T$. (EquivRel $1$,$2$:$T$. $1$ $E$ $2$) $\Rightarrow$ ($x$ ($E$$^{\mbox{\scriptsize $\ast$}}$) $y$) $\Rightarrow$ ($x$ $E$ $y$)